(include-book "../include/src/io-utilities")
(include-book "../src/acl2/cell")
(include-book "../src/acl2/state-writer")
(include-book "generators/grid-data-generator")


;;used by cells->chrs*-generates-correct-strings
;;given a list of x coords and a list of y coords that are both the same
;;length, create a list of cells that use respective x and y from each list
;;in order
(defun ints->cells (xs ys)
  (if (not xs)
      nil
      (cons (cell (car xs) (car ys)) (ints->cells (cdr xs) (cdr ys)))))


;;used by cells->chrs*-generates-correct-strings
;;given a list of x coords and a list of y coords that are the same length,
;;create list of chrs "x y,x y,x y" that follows the format for the
;;statefile
(defun int-lists->state-chrs (xs ys)
  (if (not xs)
      nil
      (append (str->chrs (rat->str (car xs) 0))
            (append '(#\Space) 
                    (append (str->chrs (rat->str (car ys) 0))
                            (append (if (cdr xs) '(#\,) nil)
                                    (int-lists->state-chrs
                                     (cdr xs) (cdr ys))))))))



;;round trip property test for cells->chrs*
;;we randomly create x and y coords but we keep track of them
;;to make sure the string created by cells->chrs* is correct
(defproperty cells->chrs*-generates-correct-strings
  (          list-size :value (random-natural)
             xs :value (random-list-of (random-integer) :size list-size)
             ys :value (random-list-of (random-integer) :size list-size))
  (equal (int-lists->state-chrs xs ys) (cells->chrs* (ints->cells xs ys))))

                                  